Property Specification Language Tutorial
Previous: What is an assertion language?| Next: Anatomy of a PSL Assertion (contd.)
Anatomy of a PSL assertion
A quick start example.
Figure 1: Anatomy of a PSL assertion.
Figure 1 shows various pieces that comprise a complete PSL assertion. The next
sections delve into individual pieces.
Label
PSL allows optional label to be specified for every assertion. It is a recommended
practice to use a meaningful name to each assertion. It helps in identifying any
failures, success reports coming from a PSL aware tool.
Verification directive
PSL provides a rich set of constructs to build complex properties. A property by
definition is a declaration and a verification tool doesn’t know what to do with
it unless told otherwise. A Verification directive sits on top of a property and
instructs a tool (simulator or a model checker) whether to "check" that the
property is never violated, or "look for occurrence of the property" etc.
When to check?
As part of the temporal layer, PSL provides means to specify "when to check for a
property". Loosely speaking they can also be called as 'occurrence operators'.
PSL supports the following occurrence operators:
- always
- never
- eventually!
- next (family of them).
The always operator is the most frequently used one and it specifies that
the following property expression should be checked every clock.
Previous: What is an assertion language?
| Next: Anatomy of a PSL Assertion (contd.)
|
